(declare-fun def () Real)
(declare-fun pv5 () Int)
(declare-fun uudefuse () (Array Int (Array Int Real)))
(declare-fun use () Real)
(declare-fun xinitumeanudefuse () (Array Int Real))
(declare-fun xinitunoiseudefuse () (Array Int Real))
(declare-fun zudefuse () (Array Int (Array Int Real)))
(declare-fun uniformuinturnd (Int Int) Int)
(declare-fun sum (Int Int Real) Real)
(declare-fun trans ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun inv ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun tptpummul ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun tptpumadd ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun tptpumsub ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun tptpuconstuarray1 (Int Real) (Array Int Real))
(declare-fun tptpuconstuarray2 (Int Int Real) (Array Int (Array Int Real)))
(assert (forall ((Xu0 Int) (Cu1 Int)) (=> (= Xu0 0) (<= (uniformuinturnd Cu1 Xu0) Xu0))))
(assert (forall ((Xu2 Int) (Cu3 Int)) (=> (>= Xu2 0) (>= (uniformuinturnd Cu3 Xu2) 0))))
(assert (exists ((Iu4 Int) (Lu5 Int) (Valu7 Real)) (xor (> Lu5 Iu4) (= (select (tptpuconstuarray1 0 Valu7) Iu4) Valu7))))
(assert (forall ((Iu8 Int) (L1u9 Int) (U1u10 Int) (Ju11 Int) (Valu14 Real)) (=> (or (<= L1u9 Iu8) (< Iu8 U1u10)) (distinct (select (select (tptpuconstuarray2 0 0 Valu14) Iu8) Ju11) Valu14))))
(assert (forall ((I0u15 Int) (J0u16 Int) (Au17 (Array Int (Array Int Real))) (Bu18 (Array Int (Array Int Real))) (Nu19 Int)) (let ((vu0 (tptpummul Au17 (tptpummul Bu18 (trans Au17))))) (= (select (select vu0 I0u15) J0u16) (select (select vu0 J0u16) I0u15)))))
(assert (forall ((I0u20 Int) (J0u21 Int) (Iu22 Int) (Ju23 Int) (Au24 (Array Int (Array Int Real))) (Bu25 (Array Int (Array Int Real))) (Mu27 Int)) (let ((vu0 (tptpummul Au24 (tptpummul Bu25 (trans Au24))))) (and (and (>= Ju23 0) (< Ju23 Mu27) (= (select (select Bu25 Iu22) Ju23) (select (select Bu25 Ju23) Iu22))) (= 0 (select (select vu0 J0u21) I0u20))))))
(assert (forall ((Iu28 Int) (Ju29 Int) (Au30 (Array Int (Array Int Real))) (Bu31 (Array Int (Array Int Real))) (Nu32 Int)) (let ((vu0 (tptpumadd Au30 Bu31))) (= (and (= (select (select Bu31 Iu28) Ju29) (select (select Bu31 Ju29) Iu28))) (= (select (select vu0 Iu28) Ju29) (select (select vu0 Ju29) Iu28))))))
(assert (exists ((Iu33 Int) (Ju34 Int) (Au35 (Array Int (Array Int Real))) (Bu36 (Array Int (Array Int Real))) (Nu37 Int)) (let ((vu0 (tptpumsub Au35 Bu36))) (=> (and (and (and (and (and (> Iu33 0) (<= Iu33 Nu37)) (>= Ju34 0)) (<= Ju34 Nu37)) (= (select (select Au35 Iu33) Ju34) (select (select Au35 Ju34) Iu33))) (= (select (select Bu36 Iu33) Ju34) (select (select Bu36 Ju34) Iu33))) (= (select (select vu0 Iu33) Ju34) (select (select vu0 Ju34) Iu33))))))
(assert (exists ((Iu38 Int) (Ju39 Int) (Au40 (Array Int (Array Int Real))) (Nu41 Int)) (let ((vu0 (trans Au40))) (xor (and (and (and (or (>= Iu38 0) (<= Iu38 Nu41)) (= Ju39 0)) (<= Ju39 Nu41)) (= (select (select Au40 Iu38) Ju39) (select (select Au40 Ju39) Iu38))) (= (select (select vu0 Iu38) Ju39) (select (select vu0 Ju39) Iu38))))))
(assert (exists ((Iu42 Int) (Ju43 Int) (Au44 (Array Int (Array Int Real))) (Nu45 Int)) (let ((vu0 (inv Au44))) (=> (and (and (or (and (>= Iu42 0) (<= Iu42 Nu45)) (>= Ju43 0)) (<= Ju43 Nu45)) (= (select (select Au44 Iu42) Ju43) (select (select Au44 Ju43) Iu42))) (= (select (select vu0 Iu42) Ju43) (select (select vu0 Ju43) Iu42))))))
(assert (forall ((I0u46 Int) (J0u47 Int) (Au50 (Array Int (Array Int Real))) (Bu51 (Array Int (Array Int Real))) (Cu52 (Array Int (Array Int Real))) (Du53 (Array Int (Array Int Real))) (Eu54 (Array Int (Array Int Real))) (Fu55 (Array Int (Array Int Real))) (Mu57 Int)) (let ((vu0 (tptpumadd Au50 (tptpummul Bu51 (tptpummul (tptpumadd (tptpummul Cu52 (tptpummul Du53 (trans Cu52))) (tptpummul Eu54 (tptpummul Fu55 (trans Eu54)))) (trans Bu51)))))) (= (and (distinct (select (select Fu55 I0u46) J0u47) (select (select Fu55 J0u47) I0u46))) (= (select (select vu0 I0u46) J0u47) (select (select vu0 J0u47) I0u46))))))
(assert (forall ((Bodyu58 Real)) (= (sum 0 (- 1) Bodyu58) 0.0)))
(assert (not (= def use)))
(assert (not (=> (and (and (and (and (and (and (and (and (and (and (and (or (and (and (and (and (and (distinct (select xinitumeanudefuse 1) use)) (= (select xinitumeanudefuse 2) use)) (= (select xinitumeanudefuse 3) use)) (distinct (select xinitumeanudefuse 4) use)) (= (select xinitumeanudefuse 5) use)) (= (select xinitunoiseudefuse 0) use)) (= (select xinitunoiseudefuse 1) use)) (= (select xinitunoiseudefuse 2) use)) (= (select xinitunoiseudefuse 3) use)) (= (select xinitunoiseudefuse 4) use)) (= (select xinitunoiseudefuse 5) use)) (>= pv5 0)) (<= pv5 (- 999 1))) (forall ((Au59 Int) (Bu60 Int)) (=> (or (and (and (<= Au59 0) (>= Bu60 0)) (<= Au59 2)) (= Bu60 pv5)) (= (select (select uudefuse Au59) Bu60) use)))) (forall ((Cu61 Int) (Du62 Int)) (xor (or (and (or (>= Cu61 0) (>= Du62 0)) (<= Cu61 2)) (<= Du62 pv5)) (= (select (select zudefuse Cu61) Du62) use)))) (forall ((Eu63 Int) (Fu64 Int)) (=> (and (and (and (>= Eu63 0) (distinct Fu64 0)) (< Eu63 2)) (= Fu64 (- pv5 1))) (= (select (select uudefuse Eu63) Fu64) use)))) (forall ((Gu65 Int) (Hu66 Int)) (=> (and (and (or (= Gu65 0) (>= Hu66 0)) (<= Gu65 2)) (<= Hu66 (- pv5 1))) (= (select (select zudefuse Gu65) Hu66) use)))) (forall ((Iu67 Int) (Ju68 Int)) (=> (and (and (and (>= Iu67 0) (>= Ju68 0)) (<= Iu67 2)) (<= Ju68 (- (+ 1 pv5) 1))) (distinct (select (select uudefuse Iu67) Ju68) use))))))
(check-sat)
